$\forall$$T$:Type, ${\it eq}$:EqDecider($T$), $L$:($T$ List).
\\[0ex]no\_repeats($T$;remove{-}repeats(${\it eq}$;$L$)) \& ($\forall$$a$:$T$. ($a$ $\in$ remove{-}repeats(${\it eq}$;$L$)) $\Leftarrow\!\Rightarrow$ ($a$ $\in$ $L$))